(set-logic QF_BVDTLIAFS)
(set-info :status unsat)
(set-option :produce-models true)
(set-option :sets-ext true)
(declare-datatype Color ((Red) (Green) (Blue)))
(declare-fun A () (Set Color))
(declare-fun B () (Set Color))
(assert (> (set.card A) (set.card B) ))
(assert (set.member Red B))
(declare-fun d () Color)
(assert (not (= d Red)))
(assert (set.member d B))
(assert (not (set.member Green A)))
(check-sat)
